#include "llvm/Pass.h"
#include "llvm/Function.h"
#include "llvm/Instruction.h"
#include "llvm/Instructions.h"
#include "llvm/Constant.h"
#include "llvm/User.h"
#include "llvm/Value.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/InstIterator.h"
#include <vector>
#include <map>
#include <string>

using namespace llvm;





typedef struct inequality_graph_node {
 Value *val;
 bool is_phi;
} node;

class constraint_desc {
  public:
   constraint_desc() {isAnInsertedCheck = false;isAnIcmp = false;}
   node *first;
   node *second;
   int c;
   bool isAnInsertedCheck;
   bool isAnIcmp;
};



void printCD(constraint_desc *cd)
{
  errs() << *(cd->first->val) << "\n";

  errs() << *(cd->second->val) << "\n";


  errs() << cd->c << "\n";
}

namespace
{
typedef std::map<Instruction *, int> mmap;
typedef std::map<Instruction *, mmap> mmap1;

typedef std::map<int, bool> c_third;
typedef std::map<Instruction *, c_third> c_second;
typedef std::map<Instruction *, c_second> c_first;
typedef std::map<Instruction *, int> active_map;
class fully_redundant
{
private:
mmap1 inequality_graph;
c_first C;
active_map active;




public:
fully_redundant(mmap1 &inequality_graph_passed)
 {
   inequality_graph = inequality_graph_passed;
 }

bool demand_prove(Instruction *, Instruction *, int);
};

bool fully_redundant::demand_prove(Instruction *a, Instruction *v, int c)
{

  //   errs() << "v is " << *v << ".\n";

  //  errs() << "from point 1\n";

  errs() << "demand_prove (" << *a << " ," << *v <<  ", " << c << "\n"; 

  c_first::iterator c_it1 = this->C.find(a);
  if(c_it1 != this->C.end())
  {
    c_second::iterator c_it2 = (*c_it1).second.find(v);
    if(c_it2 != (*c_it1).second.end())
    {
      c_third::iterator c_it3;
      for(c_it3 = (*c_it2).second.begin(); c_it3 != (*c_it2).second.end(); c_it3++)
      {
        if(((*c_it3).first <= c) && ((*c_it3).second))
          return true;
        if(((*c_it3).first >= (c)) && !((*c_it3).second))
          return false;
      }
    }
  }



  // errs() << "from point 2\n";

  if((v == a) && (c >= 0))
    return true;

  // errs() << "from point 3\n";

  mmap1::iterator find_v = this->inequality_graph.find(v);
  if(find_v == this->inequality_graph.end())
    return false;

  // errs() << "from point 4\n";

  active_map::iterator act_it = this->active.find(v);
  if(act_it != this->active.end())
  {
    if(c > (*act_it).second)
      return false;
    else
      return true;
  }

  // errs() << "from point 5\n";

  std::pair<Instruction *, int> act_pair;
  act_pair.first = v;
  act_pair.second = c;   
  this->active.insert(active.begin(), act_pair);

  std::pair<Instruction *, c_second> c_pair_level1;
  c_pair_level1.first = a;
  c_pair_level1.second = c_second();
  C.insert(this->C.begin(), c_pair_level1);

  c_first::iterator c_level1_it = this->C.find(a);

  std::pair<Instruction *, c_third> c_pair_level2;
  c_pair_level2.first = v;
  c_pair_level2.second = c_third(); 
  (*c_level1_it).second.insert((*c_level1_it).second.begin(), c_pair_level2);

  c_second::iterator c_level2_it = (*c_level1_it).second.find(v);

  std::pair<int, bool> c_pair_level3;
  c_pair_level3.first = c;
  c_pair_level3.second = false;
  (*c_level2_it).second.insert((*c_level2_it).second.begin(), c_pair_level3);  

  c_third::iterator c_level3_it = (*c_level2_it).second.find(c);

  PHINode * ph = dyn_cast<PHINode>(v);
  if(ph && (ph->getNumIncomingValues() > 1))
    (*c_level3_it).second = true;
  else
    (*c_level3_it).second = false;     

  mmap1::iterator ineq_it1 = this->inequality_graph.find(v);
  mmap::iterator ineq_it2;
  for(ineq_it2 = (*ineq_it1).second.begin(); ineq_it2 != (*ineq_it1).second.end(); ineq_it2++)
  {
    Instruction *inst2 = (*ineq_it2).first;
    int d = (*ineq_it2).second;   

    if(ph && (ph->getNumIncomingValues() > 1))
      (*c_level3_it).second = ((*c_level3_it).second && this->demand_prove(a, inst2, c- d));
    else
      (*c_level3_it).second = ((*c_level3_it).second || this->demand_prove(a, inst2, c- d));
  }

  act_it = this->active.find(v);
  this->active.erase(act_it);

  // errs() << "from point 6\n";

  return (*c_level3_it).second;   
}

}


namespace {


  struct InstructionPass : public FunctionPass {
    static char ID;
    int numberOfChecksAfterAbcd;
    InstructionPass() : FunctionPass(ID) {}

    virtual bool doInitialization(Module &M)
    {
      numberOfChecksAfterAbcd = 0;
      return true;
    }

    virtual bool runOnFunction(Function &F) {
      //errs() << "InstructionPass: " << F.getName() << "\n";
      std::vector<constraint_desc *> constraint_vector;
      
      std::vector<constraint_desc *> boundsCheckConstraints;
      
      for (inst_iterator i = inst_begin(F), E = inst_end(F); i != E; ++i)
      {
      // errs() << *i << "\n";
      // errs() << "lhs = " << *i << "\n";
       Instruction *inst = &*i;
       
       switch(inst->getOpcode()) {
       
          case Instruction::Store:
               {
               // errs() << "Store instruction was " << inst->getValueName() << "\n";
                StoreInst *sinst = dyn_cast<StoreInst>(inst);
                Value *location = sinst->getPointerOperand();
                if(!dyn_cast <GetElementPtrInst>(location)) {
                                       Value *val = sinst->getValueOperand();
                                       constraint_desc *new_constraint = new constraint_desc;
                                       node *first = new node;
                                       node *second = new node;
                                       first->val = location;
                                       first->is_phi = false;
                                       second->val = val;
                                       Instruction *valinst = (Instruction *)val;
                                       if(valinst->getOpcode() == Instruction::PHI)
                                                       second->is_phi = true;
                                       else
                                                       second->is_phi = false;
                                       new_constraint->first = first;
                                       new_constraint->second = second;;
                                       new_constraint->c = 0;

                                       constraint_vector.push_back(new_constraint);
                                     } 
               }
                break;
          case Instruction::Load:
               {
               // errs() << "Load instruction was " << inst->getValueName() << "\n";
                Value *location = (dyn_cast<LoadInst>(inst))->getPointerOperand();
                if(!dyn_cast <GetElementPtrInst>(location)) {
                                       constraint_desc *new_constraint = new constraint_desc;
                                       node *first = new node;
                                       node *second = new node;
                                       first->val = inst;
                                       first->is_phi = false;
                                       second->val = location;
                                       Instruction *locationinst = (Instruction *)location;
                                       if(locationinst->getOpcode() == Instruction::PHI)
                                                       second->is_phi = true;
                                       else
                                                       second->is_phi = false;


                                       new_constraint->first = first;
                                       new_constraint->second = second;
                                       new_constraint->c = 0;
                                       constraint_vector.push_back(new_constraint);
                                     }
               }
                break;
          case Instruction::SExt:
                {
                //errs() << "sext instruction was " << *(inst->getOperand(0)) << "\n";
                Value *operand = (dyn_cast<SExtInst>(inst))->getOperand(0);
                                       constraint_desc *new_constraint = new constraint_desc;
                                       node *first = new node;
                                       node *second = new node;
                                       first->val = inst;
                                       first->is_phi = false;
                                       second->val = operand;
                                       new_constraint->first = first;
                                       new_constraint->second = second;
                                       new_constraint->c = 0;
                                       constraint_vector.push_back(new_constraint);
               }
               break;

          case Instruction::ZExt:
               {
                //errs() << "sext instruction was " << *(inst->getOperand(0)) << "\n";
                Value *operand = (dyn_cast<ZExtInst>(inst))->getOperand(0);
                                       constraint_desc *new_constraint = new constraint_desc;
                                       node *first = new node;
                                       node *second = new node;
                                       first->val = inst;
                                       first->is_phi = false;
                                       second->val = operand;
                                       new_constraint->first = first;
                                       new_constraint->second = second;
                                       new_constraint->c = 0;
                                       constraint_vector.push_back(new_constraint);
               }
               break;
        case Instruction::Add:
               {
                 User::op_iterator OprIt = inst->op_begin();
                 ConstantInt *Opr1 = dyn_cast<ConstantInt> (&*OprIt);
                 OprIt++;
                 ConstantInt *Opr2 = dyn_cast<ConstantInt> (&*OprIt);
                 if(Opr1 && !Opr2)
                           {
                             constraint_desc *new_constraint = new constraint_desc;
                             node *first = new node;
                             node *second = new node;
                             first->val = inst;
                             first->is_phi = false;
                             second->val = OprIt->get();
                             Instruction *OprInst = (Instruction *)OprIt->get();
                             if(OprInst->getOpcode() == Instruction::PHI)
                                                   second->is_phi = true;
                             else
                                                   second->is_phi = false;

                             new_constraint->first = first;
                             
                             new_constraint->second = second;
                             new_constraint->c = (dyn_cast<ConstantInt>(Opr1))->getSExtValue();
                             constraint_vector.push_back(new_constraint);
                           }
                 else if(Opr2 && !Opr1)
                           {
                             OprIt--;
                             constraint_desc *new_constraint = new constraint_desc;
                             node *first = new node;
                             node *second = new node;
                             first->val = inst;
                             first->is_phi = false;
                             second->val = OprIt->get();
                             Instruction *Oprinst = (Instruction *)OprIt->get();
                             if(Oprinst->getOpcode() == Instruction::PHI)
                                                   second->is_phi = true;
                             else
                                                   second->is_phi = false;

                             new_constraint->first = first;
                             new_constraint->second = second;
                             new_constraint->c = (dyn_cast<ConstantInt>(Opr2))->getSExtValue();
                             constraint_vector.push_back(new_constraint);
                           }

                            

                            break;
               }
        case Instruction::Sub:
               {
                 User::op_iterator OprIt = inst->op_begin();
                 ConstantInt *Opr1 = dyn_cast<ConstantInt> (&*OprIt);
                  
                 OprIt++;
                 ConstantInt *Opr2 = dyn_cast<ConstantInt> (&*OprIt);
                /* if(Opr1 && !Opr2)
                           {
                             constraint_desc *new_constraint = new constraint_desc;
                             node *first = new node;
                             node *second = new node;
                             first->val = inst;
                             first->is_phi = false;
                             second->val = OprIt->get();
                             Instruction *OprInst = (Instruction *)OprIt->get();
                             if(OprInst->getOpcode() == Instruction::PHI)
                                                   second->is_phi = true;
                             else
                                                   second->is_phi = false;

                             new_constraint->first = first;
                             
                             new_constraint->second = second;
                             new_constraint->c = Opr1->getValue();
                             constraint_vector.push_back(new_constraint);
                           }
                 else*/ if(Opr2 && !Opr1)
                           {
                             OprIt--;
                             constraint_desc *new_constraint = new constraint_desc;
                             node *first = new node;
                             node *second = new node;
                             first->val = inst;
                             first->is_phi = false;
                             second->val = OprIt->get();
                             Instruction *Oprinst = (Instruction *)OprIt->get();
                             if(Oprinst->getOpcode() == Instruction::PHI)
                                                   second->is_phi = true;
                             else
                                                   second->is_phi = false;

                             new_constraint->first = first;
                             new_constraint->second = second;
                             new_constraint->c = -((dyn_cast<ConstantInt>(Opr2))->getSExtValue());
                             constraint_vector.push_back(new_constraint);
                           }

                            

                            break;
               }
      /* case Instruction::ICmp:
              {
                CmpInst::Predicate cond = ((ICmpInst *)inst)->getSignedPredicate();
                
                switch(cond)
                       {
                         case CmpInst::ICMP_SGE:
                            {
                              User::op_iterator OprIt = inst->op_begin();
                              OprIt++;
                              ConstantInt *Opr2 = dyn_cast<ConstantInt> (&*OprIt);
                              if(Opr2)
                                   {
                                     
                                     constraint_desc *new_constraint = new constraint_desc;
                                     node *first = new node;
                                     node *second = new node;
                                     second->val = OprIt->get();
                                     second->is_phi = false;
                                     new_constraint->second = second;
                                     OprIt--;
                                     first->val = OprIt->get();
                                     first->is_phi = false; 
                                     new_constraint->first = first;
                                     new_constraint->c = 0;
                                     constraint_vector.push_back(new_constraint);
                                   }
                               break;
                            }
                          default:
                               break;
                       }       
         
              }*/
       case Instruction::ICmp:
               {

                 if(((inst->getName()).find("boundsCheck") != std::string::npos))
                 {
                   User::op_iterator op_it = inst->op_begin();
                   Value *operand1 = op_it->get();
                   op_it++;
                   Value *operand2 = op_it->get();
                   //BasicBlock *succ1 = inst->getParent()->getTerminator()->getSuccessor(0);
                   //Instruction *succ1_inst1 = &*succ1->begin();
                   //PHINode *succ1_pi1 = dyn_cast<PHINode> (succ1_inst1);
                   //if(succ1_pi1 && (succ1_pi1->getNumIncomingValues() == 1))
                   //{


                   node *first = new node;

                   node *second = new node;
                   //first->val = succ1_pi1;
                   first->val = operand1;
                   first->is_phi = false;
                   //second->val = (Instruction *)operand2; 
                   second->val = operand2; 
                   second->is_phi = false;
                   constraint_desc *new_constraint = new constraint_desc;
                   new_constraint->first = first; 
                   new_constraint->second = second; 
                   new_constraint->c = -1;
                   new_constraint->isAnInsertedCheck = true;
                   new_constraint->isAnIcmp = true;
                   boundsCheckConstraints.push_back(new_constraint);
                   //}
                   TerminatorInst *termInst = inst->getParent()->getTerminator();
                   Instruction *succ1_inst1 = termInst->getSuccessor(0)->begin();
                   PHINode *succ1_pi1 = dyn_cast<PHINode> (succ1_inst1);
                   if(succ1_pi1 && (succ1_pi1->getNumIncomingValues() == 1))
                   {
                     node *succ_first = new node;
                     node *succ_second = new node;
                     succ_first->val = succ1_pi1;
                     succ_first->is_phi = false;
                     succ_second->val = (Instruction *)operand2; 
                     succ_second->is_phi = false;
                     constraint_desc *new_constraint_succ = new constraint_desc;
                     new_constraint_succ->first = succ_first; 
                     new_constraint_succ->second = succ_second; 
                     new_constraint_succ->c = -1;
                     new_constraint_succ->isAnIcmp = true;
                     constraint_vector.push_back(new_constraint_succ);
                     /*
                     succ_first->val = succ1_pi1;
                     succ_first->is_phi = false;
                     succ_second->val = succ1_pi1->getIncomingValue(0); 
                     succ_second->is_phi = false;
                     new_constraint_succ->first = succ_first; 
                     new_constraint_succ->second = succ_second; 
                     new_constraint_succ->c = -1;
                     constraint_vector.push_back(new_constraint_succ);
                     */

                   }
                 }
                 else
                 {
                   CmpInst::Predicate cond = ((ICmpInst *)inst)->getSignedPredicate();
                   if((cond == CmpInst::ICMP_SLT)||(cond==CmpInst::ICMP_SLE))
                   {
                     Value *operands[2];
                     int num = 0;
                     for(User::op_iterator OprIt = inst->op_begin(); OprIt != inst->op_end(); OprIt++)
                       operands[num++] = *OprIt;

                     if(!isa<ConstantInt>(operands[0]))
                     {
                       if(!isa<ConstantInt>(operands[1]))
                       {
                         BasicBlock *icmp_block = inst->getParent();
                         TerminatorInst *terminator_inst = icmp_block->getTerminator();
                         BasicBlock *succ1 = terminator_inst->getSuccessor(0);
                         BasicBlock *succ2 = terminator_inst->getSuccessor(1);
                         // errs() << "succ 1 : \n" << *succ1 << "\n";

                         // errs() << "succ 2 : \n" << *succ2 << "\n";
                         //errs() << succ2->begin() << "\n";

                         Instruction *succ1_inst1 = &*succ1->begin();
                         PHINode *succ1_phi1 = dyn_cast<PHINode>(succ1_inst1);
                         if(succ1_phi1 && (succ1_phi1->getNumIncomingValues() == 1))
                         {
                           constraint_desc *new_constraint = new constraint_desc;
                           node *first = new node;;
                           node *second = new node;
                           Value *pi_op = succ1_phi1->getIncomingValue(0);
                           first->val = succ1_phi1;
                           first->is_phi = false;
                           second->val = pi_op;
                           second->is_phi = false;
                           new_constraint->first = first;
                           new_constraint->second = second;
                           new_constraint->c = 0;
                           new_constraint->isAnIcmp = true;

                           //  errs() << *(new_constraint->first->val) << "\n";

                           //  errs() << *(new_constraint->second->val) << "\n";


                           constraint_vector.push_back(new_constraint);


                           Instruction *succ1_inst2 = &*(++(succ1->begin()));
                           PHINode *succ1_phi2 = dyn_cast<PHINode>(succ1_inst2);
                           if(succ1_phi2 && (succ1_phi2->getNumIncomingValues() == 1))
                           {

                             constraint_desc *new_constraint1 = new constraint_desc;
                             node *first1 = new node;
                             node *second1 = new node;
                             Value *pi_op1 = succ1_phi2->getIncomingValue(0);
                             first1->val = succ1_phi2;
                             first1->is_phi = false;
                             second1->val = pi_op1;
                             second1->is_phi = false;
                             new_constraint1->first = first1;
                             new_constraint1->second = second1;
                             new_constraint1->c = 0;
                             new_constraint1->isAnIcmp = true;


                             //  errs() << *(new_constraint1->first->val) << "\n";
                             //  errs() << *(new_constraint1->second->val) << "\n";

                             constraint_vector.push_back(new_constraint1);


                             constraint_desc *new_constraint2 = new constraint_desc;
                             new_constraint2->first = first;
                             new_constraint2->second = first1;
                             new_constraint2->c = 0;
                             new_constraint2->isAnIcmp = true;


                             // errs() << *(new_constraint2->first->val) << "\n";

                             // errs() << *(new_constraint2->second->val) << "\n";

                             constraint_vector.push_back(new_constraint2);
                           }
                         }

                         if(succ2)
                         {
                           Instruction *succ2_inst1 = &*succ2->begin();
                           PHINode *succ2_phi1 = dyn_cast<PHINode>(succ2_inst1);
                           if(succ2_phi1 && (succ2_phi1->getNumIncomingValues() == 1))
                           {
                             constraint_desc *new_constraint3 = new constraint_desc;
                             node *first2 = new node;
                             node *second2 = new node;
                             Value *pi_op2 = succ2_phi1->getIncomingValue(0);
                             first2->val = succ2_phi1;
                             first2->is_phi = false;
                             second2->val = pi_op2;
                             second2->is_phi = false;
                             new_constraint3->first = first2;
                             new_constraint3->second = second2;
                             new_constraint3->c = 0;
                             new_constraint3->isAnIcmp = true;


                             // errs() << *(new_constraint3->first->val) << "\n";

                             // errs() << *(new_constraint3->second->val) << "\n";

                             constraint_vector.push_back(new_constraint3);


                             Instruction *succ2_inst2 = &*(++(succ2->begin()));
                             PHINode *succ2_phi2 = dyn_cast<PHINode>(succ2_inst2);
                             if(succ2_phi2 && (succ2_phi2->getNumIncomingValues() == 1))
                             {

                               constraint_desc *new_constraint4 = new constraint_desc;
                               node *first3 = new node;
                               node *second3 = new node;
                               Value *pi_op3 = succ2_phi2->getIncomingValue(0);
                               first3->val = succ2_phi2;
                               first3->is_phi = false;
                               second3->val = pi_op3;
                               second3->is_phi = false;
                               new_constraint4->first = first3;
                               new_constraint4->second = second3;
                               new_constraint4->c = 0;
                               new_constraint4->isAnIcmp = true;


                               // errs() << *(new_constraint4->first->val) << "\n";

                               // errs() << *(new_constraint4->second->val) << "\n";

                               constraint_vector.push_back(new_constraint4);


                               constraint_desc *new_constraint5 = new constraint_desc;
                               new_constraint5->first = first3;
                               new_constraint5->second = first2;
                               new_constraint5->c = -1;
                               new_constraint5->isAnIcmp = true;


                               //errs() << *(new_constraint5->first->val) << "\n";

                               //errs() << *(new_constraint5->second->val) << "\n";

                               constraint_vector.push_back(new_constraint5);
                             }
                           }
                         }
                       }
                       else
                       {

                         BasicBlock *icmp_block = inst->getParent();
                         TerminatorInst *terminator_inst = icmp_block->getTerminator();
                         BasicBlock *succ1 = terminator_inst->getSuccessor(0);
                         BasicBlock *succ2 = terminator_inst->getSuccessor(1);
                         Instruction *succ1_inst1 = &*succ1->begin();

                         PHINode *succ1_phi1 = dyn_cast<PHINode>(succ1_inst1);
                         if(succ1_phi1 && (succ1_phi1->getNumIncomingValues() == 1))
                         {
                           constraint_desc *new_constraint = new constraint_desc;
                           node *first = new node;
                           node *second = new node;
                           Value *pi_op = succ1_phi1->getIncomingValue(0);
                           first->val = succ1_phi1;
                           first->is_phi = false;
                           second->val = pi_op;
                           second->is_phi = false;
                           new_constraint->first = first;
                           new_constraint->second = second;
                           new_constraint->c = 0;
                           new_constraint->isAnIcmp = true;


                           //errs() << *(new_constraint->first->val) << "\n";

                           //errs() << *(new_constraint->second->val) << "\n";

                           constraint_vector.push_back(new_constraint);

                           constraint_desc *new_constraint1 = new constraint_desc;
                           node *second1 = new node;
                           second1->val = operands[1];
                           second1->is_phi = false;
                           new_constraint1->first = first;
                           new_constraint1->second = second1;
                           new_constraint1->c = 0;
                           new_constraint1->isAnIcmp = true;


                           //errs() << *(new_constraint1->first->val) << "\n";

                           //errs() << *(new_constraint1->second->val) << "\n";

                           constraint_vector.push_back(new_constraint1);

                           if(succ2)
                           {
                             Instruction *succ2_inst1 = &*succ2->begin();
                             PHINode *succ2_phi1 = dyn_cast<PHINode>(succ2_inst1);
                             if(succ2_phi1 && (succ2_phi1->getNumIncomingValues() == 1))
                             {

                               constraint_desc *new_constraint2 = new constraint_desc;
                               node *first2 = new node;
                               node *second2 = new node;
                               Value *pi_op2 = succ2_phi1->getIncomingValue(0);
                               first2->val = succ2_phi1;
                               first2->is_phi = false;
                               second2->val = pi_op2;
                               second2->is_phi = false;
                               new_constraint2->first = first2;
                               new_constraint2->second = second2;
                               new_constraint2->c = 0;
                               new_constraint2->isAnIcmp = true;


                               //errs() << *(new_constraint->first->val) << "\n";

                               //errs() << *(new_constraint->second->val) << "\n";

                               constraint_vector.push_back(new_constraint2);
                             }
                           }
                         }

                       }
                     }
                   }
                 }
               }

       case Instruction::PHI:
               {
                 PHINode * phiinst = (PHINode *)inst;
                 int numincomingvalues = phiinst->getNumIncomingValues();
                 if(numincomingvalues > 1)
                 {
                   int k;
                   for(k=0; k < numincomingvalues; k++)
                   {
                     Value *val = phiinst->getIncomingValue(k);
                     constraint_desc *new_constraint = new constraint_desc;
                     node *first = new node;
                     node *second = new node;
                     first->val = inst;
                     first->is_phi = true;
                     second->val = val;
                     second->is_phi = false;
                     new_constraint->first = first;
                     new_constraint->second = second;
                     new_constraint->c = 0;
                     constraint_vector.push_back(new_constraint);
                   }
                 }
                 /* else if(numincomingvalues == 1)
                    {
                    i++;
                    Instruction* next_inst = &*i;
                    if(next_inst->getOpcode() == Instruction::PHI)
                    {
                    PHINode *phiinst1 = (PHINode *)next_inst;
                    int numincomingvaluesnext = phiinst1->getNumIncomingValues();
                    if(numincomingvaluesnext == 1)
                    {
                    Value *val = phiinst->getIncomingValue(0);
                    constraint_desc *new_constraint = new constraint_desc;
                   node *first = new node;
                   node *second = new node;
                   first->val = inst;
                   first->is_phi = false;
                   second->val = val;
                   second->is_phi = false;
                   new_constraint->first = first;
                   new_constraint->second = second;
                   new_constraint->c = 0;
                   constraint_vector.push_back(new_constraint);

                   Value *val1 = phiinst1->getIncomingValue(0);
                   constraint_desc *new_constraint1 = new constraint_desc;
                   node *first1 = new node;
                   node *second1 = new node;
                   first1->val = next_inst;
                   first1->is_phi = false;
                   second1->val = val1;
                   second1->is_phi = false;
                   new_constraint1->first = first1;
                   new_constraint1->second = second1;
                   new_constraint1->c = 0;
                   constraint_vector.push_back(new_constraint1);
                   constraint_desc *new_constraint2 = new constraint_desc;
                   node *first2 = new node;
                   node *second2 = new node;
                   first2->val = inst;
                   first2->is_phi = false;
                   second2->val = next_inst;
                   second2->is_phi = false;
                   new_constraint2->first = first;
                   new_constraint2->second = second;
                   new_constraint2->c = 0;
                   constraint_vector.push_back(new_constraint2);
                   }
                   else
                   {
                   Value *val = phiinst->getIncomingValue(0);
                   constraint_desc *new_constraint = new constraint_desc;
                   node *first = new node;
                   node *second = new node;
                   first->val = inst;
                   first->is_phi = false;
                   second->val = val;
                   second->is_phi = false;
                   new_constraint->first = first;
                   new_constraint->second = second;
                   new_constraint->c = 0;
                   constraint_vector.push_back(new_constraint);

                // BasicBlock *pblock = inst->getParent();
                // BasicBlock *predblock = pblock->getUniquePredecessor();

                // for(BasicBlock::iterator in_it = predblock->begin(); in)

                i--;
                } 
                }
                else
                {
                  Value *val = phiinst->getIncomingValue(0);
                  constraint_desc *new_constraint = new constraint_desc;
                  node *first = new node;
                  node *second = new node;
                  first->val = inst;
                  first->is_phi = false;
                  second->val = val;
                  second->is_phi = false;
                  new_constraint->first = first;
                  new_constraint->second = second;
                  new_constraint->c = 0;
                  constraint_vector.push_back(new_constraint);
                  i--;
                }
              }*/


              break;
              }
       default:
              break;
       }
      }

      /* for (User::op_iterator b = i->op_begin(), e = i->op_end(); b != e; ++b) {
         Value *operand = *b;
         errs() << "operand = " << *operand << "\n"; 
         }*/
      typedef std::map<Instruction *, int> mapin;         
      std::map<Instruction *, mapin> inequality_graph;
      std::vector<constraint_desc *>::iterator it;
      for (it = constraint_vector.begin(); it != constraint_vector.end(); it++)
      {
      //  printCD(*it);
        std::map<Instruction *, mapin>::iterator map_it;
        map_it = inequality_graph.find((Instruction *)((*it)->first->val));
        if(map_it != inequality_graph.end())
        {
          // errs() << "came here\n"; 
          std::pair<Instruction *, int> entry;
          entry.first = (Instruction *)((*it)->second->val);
          entry.second = (*it)->c;
          ((*map_it).second).insert(((*map_it).second).begin(), entry);
        }
        else
        {
          std::pair<Instruction *, mapin> outer_entry;
          outer_entry.first = (Instruction *)((*it)->first->val);
          outer_entry.second = mapin();
          inequality_graph.insert(inequality_graph.begin(), outer_entry);
          map_it = inequality_graph.find((Instruction *)((*it)->first->val));
          // if(map_it != inequality_graph.end())
          //                        errs() << "was found\n";
          std::pair<Instruction *, int> inner_entry;
          inner_entry.first = (Instruction *)((*it)->second->val);
          inner_entry.second = (*it)->c;
          ((*map_it).second).insert(((*map_it).second).begin(), inner_entry);


        }

        //  errs() << "u = " << *((*it)->first->val) << " " << ",v = " << *((*it)->second->val) << " " << ",c = " << (*it)->c << "\n" ;
      } 

      std::map<Instruction *, mapin>::iterator outer_it;
      for (outer_it = inequality_graph.begin(); outer_it != inequality_graph.end(); outer_it++)
      {
        errs() << "We are traversing the adjacency list of " << *((*outer_it).first) << "...\n";
        std::map<Instruction *, int>::iterator inner_it;
        for (inner_it = ((*outer_it).second).begin(); inner_it != ((*outer_it).second).end(); inner_it++)
        {
         errs() << "Node is " << *((*inner_it).first) << " and c is " << (*inner_it).second << " . \n";
        }
      }


      fully_redundant fred_check(inequality_graph);
      numberOfChecksAfterAbcd+=boundsCheckConstraints.size();
      int checksRemoved =0 ;
      for (it = constraint_vector.begin(); it != constraint_vector.end(); it++)
      {
        //if((*it)->isAnInsertedCheck)
        //{
       
        if ((*it)->isAnIcmp == false)
          continue;

        Instruction *v = (Instruction *)((*it)->first->val);
        Instruction *a = (Instruction *)((*it)->second->val);
        int c = (*it)->c;

        errs() << *v << " - " << *a << " <= " << c << "\n";

          if(fred_check.demand_prove(a, v, c)){ 
              if ((*it)->isAnInsertedCheck == true)
              {
                errs() << *v << " - " << *a << " <= " << c << "  was detected as redundant. \n";
                checksRemoved++;
              }
          }

          /*else
            errs() << *v << " - " << *a << " <= " << c << "  was not detected as redundant. \n";

  */
          //}
        }

        numberOfChecksAfterAbcd-=checksRemoved;
        return false;
      }
      virtual bool doFinalization(Module &M)
      {
        errs() << "The remaining checks after ABCD is " << numberOfChecksAfterAbcd << "\n";
        return true;
      }
    };

    char InstructionPass::ID = 0;
    static RegisterPass<InstructionPass> X("instructionPass", "Instruction Pass", false, false);
  }

  static void printInst(Instruction* i)
  {
    errs() << *i << "\n";
  }
  static void printBB(BasicBlock* b)
  {
    errs() << *b << "\n";
  }

    /* namespace llvm
     {
     InstructionPass *createInstructionPass();
     InstructionPass *createInstructionPass()
     {
     return new InstructionPass();
     }

     }
     */
